\begin{tabbing}
$M$:$k$ may not read $x$
\\[0ex]$\,\equiv$$_{\mbox{\scriptsize def}}$$\;\;$\=$x$ $\in$ dom(($M$.2.2.2.2.2.2.2.2.2.2).1)\+
\\[0ex]$\wedge_{b}$ ($\neg_{b}$deq{-}member(KindDeq;$k$;($M$.2.2.2.2.2.2.2.2.2.2).1($x$)))
\-
\end{tabbing}